n, k:, c:(nk).
p:(k( List)).
sum(||p(j)|| | j < k) = n  
& (j:k, x, y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
& (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j  ) 

latex

Definitions

True, T, hd(l), i<j, ij, P  Q, Dec(P), b, b, , Unit, {T}, SQType(T), S  T, i=j, if b t else f fi, P  Q, P  Q, l[i], ||as||, i  j < k, S  T, Prop, x. t(x), sum(f(x) | x < k), , t  T, x:A. B(x), P  Q, ij, {i..j}, A & B, P & Q, x:A. B(x), False, A, AB, i>j

Lemmas

ge wf, nat properties, nat wf, length wf2, sum wf, int seg wf, gt wf, select wf, length wf1, le wf, sum constant, ifthenelse wf, eq int wf, sum functionality, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bool wf, bnot wf, not wf, assert wf, sum-ite, singleton support sum, decidable int equal, squash wf, true wf, select cons tl, nat sq